Các định lý bất toàn của Gödel là hai định lý nổi tiếng về logic toán học mô tả về giới hạn vốn có của mọi hệ thống tiên đề hình thức có khả năng mô hình hóa số học cơ bản. Những định lý được Kurt Gödel xuất bản vào năm 1931, rất quan trọng trong logic toán học và triết học của toán học. Những định lý này dược diễn giải rộng rãi nhưng không phải phổ quát, rằng mục tiêu chương trình Hilbert nhằm tìm một hệ tiên đề hoàn chỉnh và nhất quán cho toàn bộ toán học là điều không tưởng.Định lý bất toàn đầu tiên đã xác định rằng không có hệ thống nhất quán các tiên đề nào mà các định lý của nó có thể được liệt kê bằng một thủ tục hiệu quả (nói cách khác là một thuật toán) lại có thể chứng minh tất cả các sự thật về việc tính toán của các số tự nhiên. Đối với bất kỳ hệ thống hình thức nhất quán nào, sẽ luôn có các mệnh đề về các số tự nhiên là đúng, nhưng không thể chứng minh được bằng hệ thống này. Định lý bất toàn thứ hai là mở rộng của định lý bất toàn thứ nhất, chứng minh rằng hệ thống đó không thể chứng tỏ được chính tính nhất quán của mình.Sử dụng tranh luận đường chéo của Cantor, các định lý bất toàn của Gödel là hai trong số những định lý đầu tiên có mối liên hệ gần gũi với sự giới hạn của các hệ thống chính thức. Các định lý này được nối tiếp bởi định lý bất khả định của Tarski về sự bất khả định hình thức của sự thật, định lí của Alonzo Church rằng Entscheidungsproblem của David Hilbert là không thể giải quyết được và định lý của Alan Turing rằng không có thuật toán nào để giải quyết các Bài toán dừng.